COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%ysp[w88,jmc]		Another attack on the Yale shooting problem
C00003 00003	Propositional version
C00004 00004	Quantified version
C00006 00005	Situation calculus version (with minimal other quantification)
C00008 00006
C00009 ENDMK
C⊗;
%ysp[w88,jmc]		Another attack on the Yale shooting problem
Old version with unintended models

holds(p,s) ∧ persistent p ∧ ¬ab1(p,e,s) ⊃ holds(p,r(e,s))

persistent alive
persistent loaded

holds(loaded,r(load,s))
holds(loaded,s) ⊃ ¬holds(alive,r(shoot,s))

holds(alive,S0)

Propositional version

¬ul* ∧ ul ⊃ ab1
ul* ⊃ ul

¬shoot* ∧ shoot ⊃ ab2
shoot* ⊃ shoot

¬heartattack* ∧ heartattack ⊃ ab3
heartattack* ⊃ heartattack

¬ul*
shoot*
¬heartattack*

shoot ∧ ¬ul ∧ ¬ab4 ⊃ ¬alive ∧ ¬ab17

heartattack ∧ ¬ab5 ⊃ ¬alive ∧ ¬ab17

¬ab17 ∧ ¬shoot ∧ ¬heartattack ⊃ alive


Quantified version

∀prop.¬asserted prop ∧ holds prop ⊃ ab(prop)
∀prop.asserted prop ⊃ holds prop

¬asserted ul
asserted shoot
¬asserted heartattack

holds heartattack ∧ ¬ab6 ⊃ fatalheartattack

holds shoot  ∧ ¬holds ul ⊃ shotfred

killfred shotfred
killfred fatalheartattack
¬killfred unload

∀prop.[killfred prop ∧ holds prop ∧ ¬ab1(prop) ⊃ ¬alive ∧ ¬ab17]

¬ab17 ∧ [∀prop.killfred prop ⊃ ¬holds prop] ⊃ alive


Situation calculus version (with minimal other quantification)

∀prop.¬asserted prop ∧ holds prop ⊃ ab(prop)
∀prop.asserted prop ⊃ holds prop
These two axioms are just as in the non situation calculus version.

∀s.¬asserted occurs(unload,s)
∀s.¬asserted occurs(heartattack,s)
∀s.asserted occurs(shoot,s) ≡ s = r(wait,r(load,S0))
asserted holds holds1(alive,S0))

(∀p e s)(holds holds1(p,s) ∧ ¬alters(e,p) ∧ ¬ab1(p,e,s) 
	⊃ holds holds1(p,r(e,s)))

¬alters(wait,loaded)
¬alters(wait,alive)
¬alters(load,alive)

If the $¬alters$ axioms are to be obtained by circumscription, it
can be a circumscription done before a specific situation is
considered, because the statements don't have a situation
parameter.